l == (x l) & (y l) & (
i, j:
. i<||l|| 
j<||l|| l[i] = x l[j] = y i<j)
clarification:
strong_before(x; y; l; T)
== (x
l T) & (y l T)
== & (
i:, j:. i<||l|| j<||l|| l[i] = x T l[j] = y T i<j) | 4,23 |
l == (x l) & (y l) & (i, j:. i<||l|| j<||l|| l[i] = x l[j] = y i<j)
l T) & (y l T)
i:, j:. i<||l|| j<||l|| l[i] = x T l[j] = y T i<j)
| Definitions | l)x:A. B(x) Q |
| FDL editor aliases | strong_before |